package trabajoISW2.domain.contracts;

import java.util.Calendar;
import java.util.List;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Address;
import trabajoISW2.domain.implementations.CreditCard;
import trabajoISW2.domain.implementations.Gender;

@Inv("getUserId() >= 0")
public interface IUser {

	@Query
	public String getUserId();
	
	@Pre({"userId.compareTo(\"\") != 0 #IllegalArgumentException", "userId != null #IllegalArgumentException" })
	@Pos("getUserId().equals(userId)")
	public void  setUserId(String userId);
	
	@Query
	public String getName();
	
	@Pre({"name.compareTo(\"\") != 0 #WrongNameException", "name != null #WrongNameException" })
	@Pos("getName().equals(name)")
	public void setName(String name);
	
	@Query
	public String getSurname();
	
	@Pre({"surname.compareTo(\"\") != 0 #WrongNameException", "surname != null #WrongNameException" })
	@Pos("getSurname().equals(surname)")
	public void setSurname(String surname);
	
	@Query
	public String getEmail();
	
	@Pre({"email.compareTo(\"\") != 0 #WrongNameException", "email != null #WrongNameException" })
	@Pos("getEmail().equals(email)")
	public void setEmail(String email);
	
	@Query
	public Calendar getBirthdate();
	
	@Pre({"birthdate != null #IllegalArgumentException", "birthdate.compareTo(Calendar.getInstance()) <= 0 #IllegalArgumentException"})
	@Pos("getBirthDate().equals(birthDate)")
	public void setBirthdate(Calendar birthdate);
	
	@Query
	public Gender getGender();
	
	@Pre("g != null #IllegalArgumentException")
	@Pos("getGender().equals(g)")
	public void setGender(Gender g);
	
	@Query
	public String getPassword();
	
	@Pre({"password.length() >= 8 #WrongNameException"})
	@Pos({"getPassword().equals(password)"})
	public void setPassword(String password);
	
	@Query
	public List<Address> getAddresses();

	@Pre("addresses != null #IllegalArgumentException")
	@Pos("getAddresses().equals(addresses)")
	public void setAddresses(List<Address> addresses);
	
	@Pre({"cc !=null #IllegalArgumentException"})
	@Pos({"!getCards().contains(cc)@Pre==>getCards().size() == getCards().size()@Pre + 1 && getCards().contains(cc)",
		  "getCards().contains(cc)@Pre ==> getCards().size() == getCards().size()@Pre"})
	public void addCreditCard(CreditCard cc);
	
	@Pre({"ad !=null #IllegalArgumentException"})
	@Pos({"!getAddresses().contains(ad)@Pre==>getAddresses().size() == getAddresses().size()@Pre + 1 && getAddresses().contains(ad)",
		  "getAddresses().contains(ad)@Pre ==> getAddresses().size() == getAddresses().size()@Pre"})
	public void addAddress (Address ad);
	
	
	@Pre("cc != null")
	@Pos({"!getCards().contains(cc)@Pre ==> getCards().size() == getCards().size()@Pre",
		   "getCards().contains(cc)@Pre ==> getCards().size() == getCards().size()@Pre -1 && getCards().contains(cc)"})
	public void removeCreditCard (CreditCard cc);
	
	
	@Pre("ad != null")
	@Pos({"!getAddresses().contains(ad)@Pre ==> getAddresses().size() == getAddresses().size()@Pre",
		   "getAddresses().contains(ad)@Pre ==> getAddresses().size() == getAddresses().size()@Pre -1 && getAddresses().contains(ad)"})
	public void removeAddress (Address ad);

}
